package it.unicam.fishpass.prism;

%%
// name of the class
%class ExpressionLexer

// Set the type of exception launched by the lexical analyzer
%scanerror ExpressionParserException

// The lexer class implement this interface which consists all integer for the tokens
%implements ExpressionParserTokens

// The type used for the tokens
%int
%unicode

// To enable char counting
%char

// To enable line counting
%line

// To enable column counting
%column

// USER DEFINED CODE
%{
Object semanticValue;
	
	/**
	 * Grants access to the field containing the number of rows (PAFAS variable
	 * definitions) read at the moment from a source input.
	 * 
	 * @return current number of the rows, read from the lexer
	 */
public int linenr(){
	return yyline;
}

	/**
	 * Grants access to the field containing the number of columns (characters)
	 * read at the moment from a row of the source input.
	 * 
	 * @return current number of the character of the row, read from the
	 *         lexer
	 */
public int columnnr(){
	return yycolumn;
}

	/**
	 * Sets the line number of the lexer to the current line. As long as the
	 * lines are read individually, the lexer is restarted everytime so that the
	 * number of the row is reset to zero. This method simply overwrite the zero
	 * value with the value of the effectively read rows.
	 * 
	 * @param line
	 *            number of the read lines
	 */
public void setLinenr(int line){
	yyline = line;
}

// The token type
int token;
%}

Arc = "->"
UrgArc = "-U>"
Var = [A-Z][A-Za-z0-9]*
Num = [0-9]+
Numeric = [0-9]+"."[0-9]+
WHITE_SPACE_CHAR=[\n | \r | \r\n]
TAB = [\t\f]
Inf = "+"?"INF"
MinusInf = "-INF"

%%
"="		{return token = EQ;}
"["		{return token = LSBRACK;}
"]"		{return token = RSBRACK;}
"."		{return token = POINT;}
"true"		{return token = TRUE;}
"false"		{return token = FALSE;}
"tt"            {return token = TT;}
"ff"            {return token = FF;}
"^"		{return token = CAPS;}
"~"		{return token = TILDE;}
"<="		{return token = LEQ;}
"<"		{return token = LS;}
">="		{return token = GEQ;}
">"		{return token = GR;}
"=="	{return token = EQQ;}
"("		{return token = LBRACK;}
")"		{return token = RBRACK;}
"+"		{return token = PLUS;}
"*"		{return token = TIMES;}
"-"		{return token = MINUS;}
"/"		{return token = DIVIDE;}
"%"		{return token = MOD;}
","		{return token = COMMA;}
";"     {return token = SEMI;}
"++"	{return token = AUTOINCREMENT;}
"--"	{return token = AUTODECREMENT;}

{WHITE_SPACE_CHAR} { /* ignore */ }
{TAB} 		{yycolumn += 8; /*Correct columns numbering w.r.t. tabs*/}

//Token with a semantic value!!
{Var}		{semanticValue = yytext(); return token = VAR;}
{Num}		{semanticValue = Integer.parseInt(yytext()); return token = NUM;}

// PRISM keywords, bool, false, init, prob, true are also used by our syntax
"A" | "const" | "ctmc" | "C" | "double" | "dtmc" | "E" | "endinit" | "endmodule" | "endrewards" | "endsystem" | "formula" | "func" | "F" | "global" | "G" | "I" | "int" | "max" | "mdp" | "min" | "module" | "X" | "nondeterministic" | "Pmax" | "Pmin" | "P" | "probabilistic" | "rate" | "rewards" | "Rmax" | "Rmin" | "R" | "S" | "stochastic" | "system" | "U" | "W"  | "label" | "LOC"

// Fallback rule for other characters not matched in any rule...
  .|\n { int value = Character.codePointAt(yytext().toCharArray(), 0);
		 // U+FFFE BOM --> see
		 // http://en.wikipedia.org/wiki/Byte_order_mark
		 // U+FFFD replacement character (in a conversion a character can
		 // be unrecognized)
		 // U+2060 word joiner (Unicode)
		 // U+0000 null character
		 if (value != '\uFEFF' && value != '\uFFFE'	&& value != '\u0000')
			return token = error; 
		 }

  // Rule applied when end of file (EOF)  is reached. It simply return the EOF 
  // token defined in the parser token interface...
<<EOF>> { return token=ENDINPUT; }
